Termination w.r.t. Q proof of /tmp/tmph1Zl5f/ReverseLastInit.trs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(app(compose, f), g), x) → app(g, app(f, x))
app(reverse, l) → app(app(reverse2, l), nil)
app(app(reverse2, nil), l) → l
app(app(reverse2, app(app(cons, x), xs)), l) → app(app(reverse2, xs), app(app(cons, x), l))
app(hd, app(app(cons, x), xs)) → x
app(tl, app(app(cons, x), xs)) → xs
last → app(app(compose, hd), reverse)
init → app(app(compose, reverse), app(app(compose, tl), reverse))

Q is empty.

↳ QTRS

  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(app(compose, f), g), x) → app(g, app(f, x))
app(reverse, l) → app(app(reverse2, l), nil)
app(app(reverse2, nil), l) → l
app(app(reverse2, app(app(cons, x), xs)), l) → app(app(reverse2, xs), app(app(cons, x), l))
app(hd, app(app(cons, x), xs)) → x
app(tl, app(app(cons, x), xs)) → xs
last → app(app(compose, hd), reverse)
init → app(app(compose, reverse), app(app(compose, tl), reverse))

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(app(compose, f), g), x) → app(g, app(f, x))
app(reverse, l) → app(app(reverse2, l), nil)
app(app(reverse2, nil), l) → l
app(app(reverse2, app(app(cons, x), xs)), l) → app(app(reverse2, xs), app(app(cons, x), l))
app(hd, app(app(cons, x), xs)) → x
app(tl, app(app(cons, x), xs)) → xs
last → app(app(compose, hd), reverse)
init → app(app(compose, reverse), app(app(compose, tl), reverse))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

app(hd, app(app(cons, x), xs)) → x
app(tl, app(app(cons, x), xs)) → xs
last → app(app(compose, hd), reverse)

Used ordering:
Polynomial interpretation [25]:

POL(app(x₁, x₂)) = x₁ + x₂
POL(compose) = 0
POL(cons) = 1
POL(hd) = 1
POL(init) = 0
POL(last) = 2
POL(nil) = 0
POL(reverse) = 0
POL(reverse2) = 0
POL(tl) = 0

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(app(compose, f), g), x) → app(g, app(f, x))
app(reverse, l) → app(app(reverse2, l), nil)
app(app(reverse2, nil), l) → l
app(app(reverse2, app(app(cons, x), xs)), l) → app(app(reverse2, xs), app(app(cons, x), l))
init → app(app(compose, reverse), app(app(compose, tl), reverse))

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(app(compose, f), g), x) → app(g, app(f, x))
app(reverse, l) → app(app(reverse2, l), nil)
app(app(reverse2, nil), l) → l
app(app(reverse2, app(app(cons, x), xs)), l) → app(app(reverse2, xs), app(app(cons, x), l))
init → app(app(compose, reverse), app(app(compose, tl), reverse))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

init → app(app(compose, reverse), app(app(compose, tl), reverse))

Used ordering:
Polynomial interpretation [25]:

POL(app(x₁, x₂)) = x₁ + x₂
POL(compose) = 0
POL(cons) = 0
POL(init) = 2
POL(nil) = 0
POL(reverse) = 0
POL(reverse2) = 0
POL(tl) = 0

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(app(compose, f), g), x) → app(g, app(f, x))
app(reverse, l) → app(app(reverse2, l), nil)
app(app(reverse2, nil), l) → l
app(app(reverse2, app(app(cons, x), xs)), l) → app(app(reverse2, xs), app(app(cons, x), l))

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(app(compose, f), g), x) → app(g, app(f, x))
app(reverse, l) → app(app(reverse2, l), nil)
app(app(reverse2, nil), l) → l
app(app(reverse2, app(app(cons, x), xs)), l) → app(app(reverse2, xs), app(app(cons, x), l))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

app(app(app(compose, f), g), x) → app(g, app(f, x))
app(app(reverse2, nil), l) → l

Used ordering:
Polynomial interpretation [25]:

POL(app(x₁, x₂)) = 1 + x₁ + x₂
POL(compose) = 2
POL(cons) = 0
POL(nil) = 0
POL(reverse) = 2
POL(reverse2) = 1

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

app(reverse, l) → app(app(reverse2, l), nil)
app(app(reverse2, app(app(cons, x), xs)), l) → app(app(reverse2, xs), app(app(cons, x), l))

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

app(reverse, l) → app(app(reverse2, l), nil)
app(app(reverse2, app(app(cons, x), xs)), l) → app(app(reverse2, xs), app(app(cons, x), l))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

app(reverse, l) → app(app(reverse2, l), nil)

Used ordering:
Polynomial interpretation [25]:

POL(app(x₁, x₂)) = x₁ + x₂
POL(cons) = 1
POL(nil) = 1
POL(reverse) = 2
POL(reverse2) = 0

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(reverse2, app(app(cons, x), xs)), l) → app(app(reverse2, xs), app(app(cons, x), l))

Q is empty.

The following Q TRS is given: Q restricted rewrite system:
The TRS R consists of the following rules:

app(app(reverse2, app(app(cons, x), xs)), l) → app(app(reverse2, xs), app(app(cons, x), l))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

app(app(reverse2, app(app(cons, x), xs)), l) → app(app(reverse2, xs), app(app(cons, x), l))

Used ordering:
Polynomial interpretation [25]:

POL(app(x₁, x₂)) = 2·x₁ + x₂
POL(cons) = 2
POL(reverse2) = 0

↳ QTRS

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ RRRPoloQTRSProof

        ↳ QTRS

          ↳ RRRPoloQTRSProof

            ↳ QTRS

              ↳ RRRPoloQTRSProof

                ↳ QTRS

                  ↳ RRRPoloQTRSProof

                    ↳ QTRS

                      ↳ RisEmptyProof

Q restricted rewrite system:
R is empty.
Q is empty.

The TRS R is empty. Hence, termination is trivially proven.